\section{Поток управления}

Будем считать, что все операторы программы имеют уникальные метки (номера). 
Обозначим множество этих меток через $L$.

$$
\ctrans{}{S_i}{\{i\}}{S_i - \llang{skip}, \mbox{ присваивание, чтение или запись}}
$$

$$
\trule{\trans{}{\inmath{S_1}}{\sigma_1},\trans{}{\inmath{S_2}}{\sigma_2}}
      {\trans{}{\llang{$S_1\;$;$\;S_2$}}{\sigma_1\sigma_2}}
$$

$$
\trule{\trans{}{\inmath{S_1}}{\sigma_1}}
      {\trans{}{\{\llang{if$\;e\;$then$\;S_1\;$else$\;S_2\;$}\}_i}{i\sigma_1}}
$$

$$
\trule{\trans{}{\inmath{S_2}}{\sigma_2}}
      {\trans{}{\{\llang{if$\;e\;$then$\;S_1\;$else$\;S_2\;$}\}_i}{i\sigma_2}}
$$

$$
\trans{}{\{\llang{while$\;e\;$do$\;S$}\}_i}{i}
$$

$$
\trule{\trans{}{\inmath{S}}{\sigma}, \trans{}{\{\llang{while$\;e\;$do$\;S$}\}_i}{\omega}}
      {\trans{}{\{\llang{while$\;e\;$do$\;S$}\}_i}{i\sigma\omega}}
$$
